* Step 1: DependencyPairs WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
f(k(a()),k(b()),X) -> f(X,X,X)
g(X) -> u(h(X),h(X),X)
h(d()) -> c(a())
h(d()) -> c(b())
u(d(),c(Y),X) -> k(Y)
- Signature:
{f/3,g/1,h/1,u/3} / {a/0,b/0,c/1,d/0,k/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,g,h,u} and constructors {a,b,c,d,k}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X),h#(X),h#(X))
h#(d()) -> c_3()
h#(d()) -> c_4()
u#(d(),c(Y),X) -> c_5()
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X),h#(X),h#(X))
h#(d()) -> c_3()
h#(d()) -> c_4()
u#(d(),c(Y),X) -> c_5()
- Weak TRS:
f(k(a()),k(b()),X) -> f(X,X,X)
g(X) -> u(h(X),h(X),X)
h(d()) -> c(a())
h(d()) -> c(b())
u(d(),c(Y),X) -> k(Y)
- Signature:
{f/3,g/1,h/1,u/3,f#/3,g#/1,h#/1,u#/3} / {a/0,b/0,c/1,d/0,k/1,c_1/1,c_2/3,c_3/0,c_4/0,c_5/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {f#,g#,h#,u#} and constructors {a,b,c,d,k}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
h(d()) -> c(a())
h(d()) -> c(b())
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X),h#(X),h#(X))
h#(d()) -> c_3()
h#(d()) -> c_4()
u#(d(),c(Y),X) -> c_5()
* Step 3: Trivial WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
g#(X) -> c_2(u#(h(X),h(X),X),h#(X),h#(X))
h#(d()) -> c_3()
h#(d()) -> c_4()
u#(d(),c(Y),X) -> c_5()
- Weak TRS:
h(d()) -> c(a())
h(d()) -> c(b())
- Signature:
{f/3,g/1,h/1,u/3,f#/3,g#/1,h#/1,u#/3} / {a/0,b/0,c/1,d/0,k/1,c_1/1,c_2/3,c_3/0,c_4/0,c_5/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {f#,g#,h#,u#} and constructors {a,b,c,d,k}
+ Applied Processor:
Trivial
+ Details:
Consider the dependency graph
1:S:f#(k(a()),k(b()),X) -> c_1(f#(X,X,X))
2:S:g#(X) -> c_2(u#(h(X),h(X),X),h#(X),h#(X))
-->_1 u#(d(),c(Y),X) -> c_5():5
-->_3 h#(d()) -> c_4():4
-->_2 h#(d()) -> c_4():4
-->_3 h#(d()) -> c_3():3
-->_2 h#(d()) -> c_3():3
3:S:h#(d()) -> c_3()
4:S:h#(d()) -> c_4()
5:S:u#(d(),c(Y),X) -> c_5()
The dependency graph contains no loops, we remove all dependency pairs.
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
h(d()) -> c(a())
h(d()) -> c(b())
- Signature:
{f/3,g/1,h/1,u/3,f#/3,g#/1,h#/1,u#/3} / {a/0,b/0,c/1,d/0,k/1,c_1/1,c_2/3,c_3/0,c_4/0,c_5/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {f#,g#,h#,u#} and constructors {a,b,c,d,k}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(1))